интуиционистская логика

        ИНТУИЦИОНИСТСКАЯ ЛОГИКА — первоначально появилась как логика интуиционистской математики, но затем область ее применения чрезвычайно расширилась. Неформально И.л. начал развивать Л. Брауэр в 1907; первую интерпретацию, независимую от интуиционистской математики, дал А.Н. Колмогоров; первую формализацию построил А. Гейтинг.

        Язык И. л. совпадает с языком классической логики. Правила естественного вывода для всех связок, кроме отрицания, также можно оставить неизменными. Для отрицания правило снятия двойного отрицания ослабляется до правила «Из лжи следует все что угодно».

        В И. л. все связки независимы. В ней нет стандартных форм, аналогичных классическим. Как правило, преобразования, связанные с законами формулировки отрицаний и приведения к предваренной форме, действуют лишь в одну сторону. Так, напр., верно -AW-B-,A8LB), а -А & В)=> -A v -£ выполнено не всегда.

        Слабый закон исключенного третьего «А и его отрицание не могут быть одновременно ложны» сохраняется и в И.л. в форме —1 —I (А V —А), отвергается как логический закон лишь (A v -А). Поэтому неправильно трактовать И. л. как вводящую дополнительные истинностные значения; она, скорее, отвергает саму концепцию логических значений. И. л. не может быть описана конечной системой логических значений.

        Для И. л. выполнено свойство корректности относительно V и 3: если доказано А V В, то доказано либо А, либо В; если доказано ЗхА(х), то для некоторого t доказано A(t). Данным свойством классическая логика не обладает. Классическая логика вкладывается в интуиционистскую. Первым такое погружение построил Гливенко.

        И. л. имеет несколько математических интерпретаций. Исторически первой была интерпретация А. Тарского. В ней значениями истинности для предикатов являются открытые подмножества топологического пространства. Значения & v3 определяются булевым образом. Значение —А есть внутренность дополнения значения А. Напр., несправедливость А V —А можно продемонстрировать следующим образом: объединение открытого единичного круга и внутренности его дополнения дает плоскость без единичной окружности. Следующей интерпретацией стала алгебраическая. Еще одна семантика И.л. берет начало от Бета и развита Крипке. Это — один из видов моделей Крипке (см. Семантика возможных миров).

        Параллельно с этим развивалась линия, ведущая начало от содержательного смысла И. л. согласно Брауэру. Формулы истолковывались как задачи, логические связки — как преобразования задач, аксиомы — как задачи, для которых решения считаются известными; правила вывода — как преобразования решений задач. Данные идеи систематизировал А.Н. Колмогоров. Каждой формуле А сопоставляется множество ее реализаций '. Каждая реализация считается решением задачи, соответствующей А.

        Реализации элементарных формул задаются по определению. ® (А & В) - ®Ах©В. ® (А V В) = ®АФ®В. ®-пА=<=>®А=0. ®ЗхА(х)=Ф_аеи®А(а). Реализациями А => В являются эффективные функционалы из ©А в ®В. Реализациями являются эффективные функционалы, перерабатывающие каждое aeU в реализацию А(а). Уникальным свойством И. л. является наличие двух разнородных и несводимых друг к другу классов семантик: реализуемостей и моделей Крипке.

        В данном определении остается не уточненным понятие эффективного функционала. В частности, если взять в качестве эффективных функционалов все классические функции, то логика превращается в классическую. С.К. Клини построил первый точный вариант реализуемости, взяв в качестве эффективных операторов алгоритмы и кодируя программы алгоритмов натуральными числами, обходя, таким образом, сложности с операторами высших типов (клиниевская реализуемость). Он показал, что из доказательства в интуиционистской арифметике извлекается клиниевская реализация доказанной теоремы и поэтому если мы доказали ЗхА(х), то имеется такое п, что доказано А(п). Это точно обосновало тезис Брауэра, что интуиционистские доказательства дают построения.

        Обобщения идеи Колмогорова на другие классы построений с ограниченными ресурсами показали, что идея конструктивности не является исключительной принадлежностью И. л. Другим классам построений соответствуют другие конструктивные логики, чаще всего противоречащие как классической логике, так и И. л. Напр., в линейных логиках не принимается закон А = > А & А, в нильпотентных А = > А влечет -А, и т. д. Поскольку разные классы построений противоречат друг другу уже на логическом уровне, то совместное их использование приводит к грубым концептуальным противоречиям и, соответственно, к нежелательным практическим эффектам. Поэтому система конструктивных логик стала основой для системы стилей программирования, а И. л. занимает в ней место логики структурного программирования.

        Аналогия между доказательствами в И. л. и построениями усилена в [1]. Замкнутые типизированные выражения в комбинаторной логике изоморфны выводам в гильбертовской формулировке импликативного фрагмента И. л. Замкнутые типизированные А. -термы изоморфны выводам в импликативном фрагменте естественного вывода. Изоморфизм между выводами и Х -термами пытались расширить на всю И. л. Но на его пути стоит препятствие, указанное еще Брауэром и явно выделенное НА. Шаниным. Выводы в И. л. соединяют построения и их обоснования. В частности, построения, проделанные при выводе -iA, нельзя вычислять, поскольку они приведут к ошибке. Такие объекты, которые нельзя или не нужно вычислять в программе, но нужно рассматривать для ее обоснования, Г. С. Цейтин назвал призраками. НА. Шанин рассмотрел алгоритм конструктивной расшифровки, разбивающий формулу на задачу и обоснование решения, причем вторая часть может в рамках конструктивного направления в математике доказываться классически. Дан алгоритм классификации объектов вывода в И. л., отделяющий построения и призраки.

        И. л. варьировали многими способами. В минимальной логике Иогансона отбрасывается ex falso quodlibet. Как оказалось, в прикладных теориях интуиционистское отрицание моделируется (напр., в теории натуральных чисел как А = > 0=1). Г р и с предложил симметрическую И. л., в которой истина и ложь равноправны. В симметрической И. л. сохраняются обычные правила формулировки отрицаний классической логики. Отрицание в ней обычно обозначается =>А, интерпретируется как задача построения контрпримера к А и называется сильным отрицанием или конструктивным опровержением. Симметрическая И. л. детально исследована в монографии И.Д. Заславского.

        Н.Н. Непейвода

        Лит.: Шанин Н.А. О конструктивном понимании математических суждений // Тр. матем. ин-та им. В. А. Стеклова. Т. 52; Непейвода Н.Н. О построении правильных программ // Вопросы кибернетики. Т. 46. 1978; Непейвода Н.Н., Скопин Н.Н. Основания программирования. Ижевск—Москва, 2003; Brouwer L.E.J. Over de grondslagen der wiskunde [Об основаниях знания]. Amsterdam — Leipzig, 1907; Brouwer L.E.J. De onbetrouwbaarheid der logische principes [О недостоверности логических принципов] // Tijdskrift. Wijsbegeerte. Vol. 2. 1908; HeytingA. Die formalen Regeln der intuitionistischen Logik // Sitz. Berlin, 1930; Колмогоров А.Н. Zur Deutung der intuition-istischen Logik // Math. Zeitschrift. Vol. 35. 1932; Tarski A. Der Aussagenkalkul und die Topologie // Fundamenta Mathematicae. Vol. 31. 193; Curry H.B. Combinatory Logic. Vol. 2. New York, 1968.